1. Field of the Invention
The invention relates in general to formal verification of a system, and more particularly, to verification of analog circuits.
2. Description of the Related Art
FIG. 1 is an illustrative drawing of flow of a typical analog circuit verification process. SPICE remains the tool of choice for analog circuit designers. The most common way of verifying analog circuits has been to run a sequence of SPICE simulations and post processing the simulation results to find if the circuit fails to meet the specifications for any of the sampled cases. Once the failing cases have been identified, the design is tweaked and the simulations redone. This process is repeated until the circuit passes all the tests. More specifically, referring to FIG. 1, a verification process 100 typically involves a loop in which a circuit netlist 102 for a design that identifies devices and nets interconnecting the devices is input to an analog simulation tool 104 such as SPICE. The SPICE simulation tool produces a circuit simulation 106, which is evaluated for compliance with circuit performance constraints. A design optimization tool 108 uses the evaluation results as a basis to modify the circuit design and its netlist. The cycle repeats until acceptable results are achieved.
In general, designers design block level circuits such as opamps and comparators, for example, and run large number of simulations to verify them. Aggressive scaling down of device dimensions due to advances in semiconductor manufacturing technologies has made these designs ever more challenging as designers need to ensure that the circuit works over wide ranges of process, voltage and temperature (PVT) conditions. The verification process of the general type described above is a very time consuming methodology with no guarantees that the circuit will work in all possible simulation scenarios that have not been tested. As a result, experienced analog circuit designers often spend a significant portion of their time designing basic circuit blocks and porting them from one technology node to another. There is a real need for a formal verification methodology that can improve circuit predictability while allowing the designers to focus on more challenging circuits.
A circuit simulation problem that SPICE solves typically involves a set of KCL (Kirchoff's Current Law) equations. See, for example, T. Quarles, The SPICE3 implementation guide, In UCB/ERL M89/44, April 1989. The current values are obtained from device models, e.g., BSIM3, V=IR relationships, etc. The Kirchoff's Voltage Law is ensured to hold by intelligently labeling the voltage nodes. SPICE performs local searches from some carefully chosen starting point via Newton-Raphson iterations to find a solution to these equations.
The primary goal of SPICE in the early phase of its development in the 1970's was to simulate a single circuit instance—with fixed width and lengths of transistors, values of parasitics, transistor model parameters, input conditions, etc. As newer, aggressive manufacturing processes were developed, the problem of designing a circuit became more challenging. Designers now often have to design circuits that should meet the specifications not only at the nominal conditions but also for many different environmental conditions (process, voltage, temperature, input stimuli, etc.) in which the circuit could operate. Thus, the circuit simulation problem has transformed into a verification problem wherein the designer is looking for some “guarantees” on the behavior of the circuits. Much work has gone into the further development of SPICE to handle these new simulation/verification scenarios, e.g., ability to handle process corners, Monte Carlo simulation, measurement description language (SpectreMDL), native simulation speed-up (Ultrasim), circuit synthesis. See, for example, A. H. Shah, S. Dugalleix, and F. Lemery High-performance CMOS-amplifier design uses front-to-back analog flow, EDN, 2002.), etc.
One problem with SPICE is that the core algorithm is geared towards solving a single simulation problem, which falls short of addressing the verification challenges of designers, finally leaving it to the designers' insight to find the failing cases. Another problem with SPICE-based circuit simulation is that the underlying core algorithm is based on local search of the solution space (Newton-Raphson). Due to the local nature of the search, it can be difficult to use SPICE to determine whether the circuit does not obey a property over a range of operating conditions. For example, a property to be checked may be whether a start up circuit always “starts-up” for a range of initial conditions.
The use of digital verification techniques for analog circuit verification has been proposed as an alternative to SPICE-based verification. Some of the earlier attempts at applying digital verification techniques to the analog domain were presented in R. P. Kurshan and K. L. McMillan, Analysis of digital circuits through symbolic reduction, IEEE Transactions on CAD, pages 1356-1371, 1991. Various tools focusing on hybrid verification have been developed that could be extended for analyzing dynamical systems representing analog circuits. See, for example, G. Frehse. Phaver: Algorithmic verification of hybrid systems past hytech, Proc. of the 5th International Workshop on Hybrid Systems: Computation and Control (HSCC), pages 258-273, 2005; E. Asarin, O. Bournez, T. Dang, and O. Maler, Approximate reachability analysis of piecewise linear dynamical systems, Hybrid Systems: Computation and Control, 2000; J. Kapinski and B. H. Krogh, Verifying switched mode computer controlled systems. In IEEE Conference on Computer-Aided Control System Design, pages 98-103, 2002; and T. A. Henzinger, P.-H. Ho, and H. Wong-Toi. HyTech: A model checker for hybrid systems Lecture Notes in Computer Science 1254, Springer-Verlag, pages 460-463, 1997.
Recently, hybrid verification techniques have been applied to verify transient properties for analog circuits. See, for example, G. Frehse, B. H. Krogh, and R. A. Rutenbar, Verifying analog oscillator circuits using forward/backward refinement, DATE, pages 257-262, 2006; S. Gupta, B. H. Krogh, and R. A. Rutenbar, Towards formal verication of analog designs, ICCAD, pages 210-217, 2004; S. Little, N. Seegmiller, D. Walter, C. Myers, and T. Yoneda, Verification of analog/mixed-signal circuits using labeled hybrid petri nets, ICCAD, 2006; and D. Walter, S. Little, and C. Myers, Bounded model checking of analog and mixed-signal circuits using an SMT solver, Automated Technology for Verification and Analysis, 2007. Unfortunately, the practicality of some of these methods is limited by the constraint on the underlying circuits to have a linear behavior. The proposed methodologies, sometimes, also require a simpler abstract model for a given circuit block that they need as a starting point. See, D. Walter et al, for example. These assumptions themselves introduce (over and under) approximations in the starting models that are used by the different verification techniques to prove properties. Since, there is a disconnect between these base models and the underlying transistor level circuits, any formal proofs on the models have limited practical usefulness.
Thus, there has been a need for improvements in techniques to verify systems over a range of properties. In particular, there has been a need for improvements in techniques to verify analog and mixed signal circuits. The present invention meets this need.